w:World, k:Knd, i:Id, t:. w-knum(w;i;k;t)   

latex

Definitions	, P & Q, i  j < k, a < b, Void, x:AB(x), P  Q, False, A, A  B, {x:A| B(x)} , , {i..j}, x:A. B(x), s = t, b, x:A  B(x), P  Q, Unit, left + right, World, Knd, Atom$n, Id, , x.A(x), x. t(x), w-knum(w;i;k;t), a(i;t), isnull(a), #$n, kind(a), a = b, b, p  q, if b then t else f fi , sum(f(x) | x < k), , t  T
Lemmas	nat wf, Id wf, Knd wf, world wf, int seg wf, sum wf, non neg sum, band wf, bnot wf, w-isnull wf, w-a wf, not wf, assert wf, bool wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, ifthenelse wf, eq knd wf, w-kind wf, le wf